#include "PDTNode.h"
#include "PDTCodeGraph.h"
#include "PDTGraphVisitor.h"
#include "PDTZ3GraphVisitor.h"

#include "PDTCondition.h"
#include "PDTBehavior.h"

PDTNode::PDTNode(PDTCodeGraph & CG) :
  Z3node(NULL)
{
  CG.addNode(this);
  id = CG.currentId;
  CG.updateCurrentId();
  nValue = NULL;
  touched = false;
}

NodeId
PDTNode::getId() const
{
  return id;
}

vector<PDTNode*> &
PDTNode::getParents()
{
  return parents;
}

vector<PDTNode*> &
PDTNode::getChildren()
{
  return children;
}

void
PDTNode::addParent(PDTNode* parent)
{
  parents.push_back(parent);
}

void
PDTNode::addChild(PDTNode* child)
{
  children.push_back(child);
}


Z3_ast
PDTNode::Z3visit(PDTZ3Visitor & ZV)
{
  if (Z3node != NULL)
    return Z3node;
  ZV.currentNode = this;
  return Z3NodeVisit(ZV);
}

void
PDTNode::traverse(PDTGraphVisitor &gv)
{
  gv.pre(this);
  //printType();cout<<endl;///visitor functions

  //vector<PDTNode*> & children = this->getChildren();

  for (unsigned int i = 0; i < children.size(); i++)
    {
      PDTNode * child = children[i];
      
      gv.beforeChild(this, child, i);      
      child->traverse(gv);
      gv.afterChild(this, child, i);
    }
  gv.post(this);
}

PDTNode::~PDTNode()
{
}


char *
PDTNode::makeUniqueName(const char * prefix)
{
  static char name[1024];
  sprintf(name,"CG_%s_ID_%d", prefix, getId());
  return name;
}

char *
PDTNode::makeIVName(const char * prefix)
{
  static char name[1024];
  sprintf(name,"CG_%s_iv_%d", prefix, getId());
  return name;
}

PDTPreCondition* 
PDTNode::
findPre(const string & spec)
{
    PDTNode * pre= NULL;
    int childSize = children.size();
    for (int i=0; i<childSize; i++)
    {
        if (children[i]->isPreCondition())
        {
            if (spec.empty()){
                pre = children[i];
                break;
            }
            PDTCondition* cond = dynamic_cast<PDTCondition*>(children[i]);
            if (cond->getName() == spec){
                pre = children[i];
                break;
            }
        }
        pre = children[i]->findPre(spec);
        if (pre != NULL) {
            break;
        }
    }
    return dynamic_cast<PDTPreCondition*>(pre);
}

PDTPostCondition* 
PDTNode::
findPost(const string & spec)
{
    PDTNode * post= NULL;
    int childSize = children.size();
    for (int i=0; i<childSize; i++)
    {
        if (children[i]->isPostCondition())
        {
            if (spec.empty()){
                post = children[i];
                break;
            }
            PDTCondition* cond = dynamic_cast<PDTCondition*>(children[i]);
            if (cond->getName() == spec){
                post = children[i];
                break;
            }
        }
        post = children[i]->findPost(spec);
        if (post != NULL) {
            break;
        }
    }
    return dynamic_cast<PDTPostCondition*>(post);
}


PDTBehaviors* 
PDTNode::
findBehaviors(const string & spec)
{
    PDTNode * bhvr= NULL;
    int childSize = children.size();
    for (int i=0; i<childSize; i++)
    {
        if (children[i]->isBehaviors())
        {
            if (spec.empty()){
                bhvr = children[i];
                break;
            }
            PDTBehaviors * bhv1= dynamic_cast<PDTBehaviors*>(children[i]);
            if (bhv1->getName() == spec){
                bhvr = children[i];
                break;
            }
        }
        bhvr = children[i]->findBehaviors(spec);
        if (bhvr != NULL) {
            break;
        }
    }
    return dynamic_cast<PDTBehaviors*>(bhvr);
}
